(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(assert v9)
(assert (not v2))
(declare-const v12 Bool)
(declare-const v13 Bool)
(assert v6)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(assert (forall ((q0 (_ BitVec 7)) (q1 (_ BitVec 4))) (=> (bvugt (_ bv78 7) (_ bv78 7)) (distinct q1 #x4 q1 #x4))))
(assert (= v10 v3 (bvult (_ bv997 10) (_ bv997 10)) v1 (not v2) v1 (or v0 (bvult (_ bv78 7) (_ bv78 7)) v3 v5 v0 v9 v5) v12 (bvult (_ bv78 7) (_ bv78 7)) (distinct ((_ repeat 2) (_ bv78 7)) ((_ repeat 2) (_ bv78 7)) ((_ repeat 2) (_ bv78 7)) ((_ repeat 2) (_ bv78 7))) (or v0 (bvult (_ bv78 7) (_ bv78 7)) v3 v5 v0 v9 v5)))
(declare-const v17 Bool)
(assert (distinct v7 v0 v10))
(declare-const v18 Bool)
(declare-const _3-0 (_ BitVec 3))
(assert (distinct #x4 #x4 #x4 #x4 #x4))
(assert (and (= ((_ repeat 2) (_ bv78 7)) ((_ repeat 2) (_ bv78 7)) ((_ repeat 2) (_ bv78 7)) ((_ repeat 2) (_ bv78 7))) (distinct (_ bv78 7) (_ bv78 7) (_ bv78 7))))
(assert (or (or v0 (bvult (_ bv78 7) (_ bv78 7)) v3 v5 v0 v9 v5) (distinct (_ bv78 7) (_ bv78 7) (_ bv78 7)) (= ((_ repeat 2) (_ bv78 7)) ((_ repeat 2) (_ bv78 7)) ((_ repeat 2) (_ bv78 7)) ((_ repeat 2) (_ bv78 7))) v7 (= v10 v3 (bvult (_ bv997 10) (_ bv997 10)) v1 (not v2) v1 (or v0 (bvult (_ bv78 7) (_ bv78 7)) v3 v5 v0 v9 v5) v12 (bvult (_ bv78 7) (_ bv78 7)) (distinct ((_ repeat 2) (_ bv78 7)) ((_ repeat 2) (_ bv78 7)) ((_ repeat 2) (_ bv78 7)) ((_ repeat 2) (_ bv78 7))) (or v0 (bvult (_ bv78 7) (_ bv78 7)) v3 v5 v0 v9 v5)) v13 v4 v15 v17 (and (= ((_ repeat 2) (_ bv78 7)) ((_ repeat 2) (_ bv78 7)) ((_ repeat 2) (_ bv78 7)) ((_ repeat 2) (_ bv78 7))) (distinct (_ bv78 7) (_ bv78 7) (_ bv78 7)))))
(assert (distinct v0 v13 v17 v4))
(check-sat)
